'''
Created on 2013-01-22

@author: levi
'''
import unittest

import time

from symbolic_state_space import SymbolicStateSpace

from t_core.matcher import Matcher
from tc_python.arule import ARule
from tc_python.frule import FRule

from transformation_patterns.HS2S import HS2S
from transformation_patterns.HM2M import HM2M
from transformation_patterns.HF2F import HF2F
from transformation_patterns.HSM2SM import HSM2SM
from transformation_patterns.HSF2SF import HSF2SF
from transformation_patterns.HMM2MM import HMM2MM
from transformation_patterns.HFF2FF import HFF2FF

from symbolic_exec_patterns.HMatch_S2SLHS import HMatch_S2SLHS
from symbolic_exec_patterns.HMatch_M2MLHS import HMatch_M2MLHS
from symbolic_exec_patterns.HMatch_F2FLHS import HMatch_F2FLHS

from symbolic_exec_patterns.HMatch_L2_SM2SM_S2SLHS import HMatch_L2_SM2SM_S2SLHS
from symbolic_exec_patterns.HMatch_L2_SM2SM_M2MLHS import HMatch_L2_SM2SM_M2MLHS
from symbolic_exec_patterns.HMatch_L2_MM2MM_M2M_1LHS import HMatch_L2_MM2MM_M2M_1LHS
from symbolic_exec_patterns.HMatch_L2_MM2MM_M2M_2LHS import HMatch_L2_MM2MM_M2M_2LHS

from property_proof.HFindPropertyIsolatedElementsLHS import HFindPropertyIsolatedElementsLHS
from property_proof.HFindPropertyConnectedElementsLHS import HFindPropertyConnectedElementsLHS
from property_proof.HFindPropertyCompleteLHS import HFindPropertyCompleteLHS

from collapse_with_backward_patterns.HFindTwoMatchElementsSameTypeLHS import HFindTwoMatchElementsSameTypeLHS
from collapse_with_backward_patterns.HFindTwoApplyElementsWithBackwardLHS import HFindTwoApplyElementsWithBackwardLHS

from collapse_with_backward_patterns.HMoveOneInputDirectMatchDiffRulesLHS import HMoveOneInputDirectMatchDiffRulesLHS
from collapse_with_backward_patterns.HMoveOneInputDirectMatchDiffRulesRHS import HMoveOneInputDirectMatchDiffRulesRHS

from collapse_with_backward_patterns.HMoveOneInputIndirectMatchDiffRulesLHS import HMoveOneInputIndirectMatchDiffRulesLHS
from collapse_with_backward_patterns.HMoveOneInputIndirectMatchDiffRulesRHS import HMoveOneInputIndirectMatchDiffRulesRHS

from collapse_with_backward_patterns.HMoveOneOutputDirectMatchDiffRulesLHS import HMoveOneOutputDirectMatchDiffRulesLHS
from collapse_with_backward_patterns.HMoveOneOutputDirectMatchDiffRulesRHS import HMoveOneOutputDirectMatchDiffRulesRHS

from collapse_with_backward_patterns.HMoveOneOutputIndirectMatchDiffRulesLHS import HMoveOneOutputIndirectMatchDiffRulesLHS
from collapse_with_backward_patterns.HMoveOneOutputIndirectMatchDiffRulesRHS import HMoveOneOutputIndirectMatchDiffRulesRHS

from collapse_with_backward_patterns.HMoveOneInputDirectApplyDiffRulesLHS import HMoveOneInputDirectApplyDiffRulesLHS
from collapse_with_backward_patterns.HMoveOneInputDirectApplyDiffRulesRHS import HMoveOneInputDirectApplyDiffRulesRHS

from collapse_with_backward_patterns.HMoveOneOutputDirectApplyDiffRulesLHS import HMoveOneOutputDirectApplyDiffRulesLHS
from collapse_with_backward_patterns.HMoveOneOutputDirectApplyDiffRulesRHS import HMoveOneOutputDirectApplyDiffRulesRHS

from collapse_with_backward_patterns.HMoveOneBackwardLinkDiffRulesLHS import HMoveOneBackwardLinkDiffRulesLHS
from collapse_with_backward_patterns.HMoveOneBackwardLinkDiffRulesRHS import HMoveOneBackwardLinkDiffRulesRHS

from collapse_with_backward_patterns.HDeleteUncollapsedElementMatchDiffRulesLHS import HDeleteUncollapsedElementMatchDiffRulesLHS
from collapse_with_backward_patterns.HDeleteUncollapsedElementMatchDiffRulesRHS import HDeleteUncollapsedElementMatchDiffRulesRHS

from collapse_with_backward_patterns.HDeleteUncollapsedElementApplyDiffRulesLHS import HDeleteUncollapsedElementApplyDiffRulesLHS
from collapse_with_backward_patterns.HDeleteUncollapsedElementApplyDiffRulesRHS import HDeleteUncollapsedElementApplyDiffRulesRHS


class Test(unittest.TestCase):

    def setUp(self):
        self.backwardPatterns = {'HS2S': None,
                                 'HM2M': None,  
                                 'HF2F': None,                 
                                 'HSM2SM': [Matcher(HMatch_S2SLHS()),Matcher(HMatch_M2MLHS())],
                                 'HMM2MM': [Matcher(HMatch_M2MLHS()),Matcher(HMatch_M2MLHS())],
                                 'HSF2SF': [Matcher(HMatch_S2SLHS()),Matcher(HMatch_F2FLHS())],
                                 'HFF2FF': [Matcher(HMatch_F2FLHS()),Matcher(HMatch_F2FLHS())]}
        

#        self.backwardPatterns2 = {'HL1_S2S': None,
#                                 'HL1_M2M': None,                   
#                                 'HL2_SM2SM': [Matcher(HMatch_L2_SM2SM_S2SLHS()),Matcher(HMatch_L2_SM2SM_M2MLHS())],
#                                 'HL2_MM2MM': [Matcher(HMatch_L2_MM2MM_M2M_1LHS()),Matcher(HMatch_L2_MM2MM_M2M_2LHS())],
#                                 'HL2_F2F': None}

    def test_verify_simple_property(self):
        transformation = [[HS2S(), HM2M(), HF2F()], [HSM2SM(), HMM2MM(), HSF2SF(), HFF2FF()]]
        rulesIncludingBackLinks = [[], [transformation[1][0], transformation[1][1], transformation[1][2], transformation[1][3]]]
        s = SymbolicStateSpace(transformation, rulesIncludingBackLinks, self.backwardPatterns)
        s.build_set()
        s.verify_property(HFindPropertyIsolatedElementsLHS(), HFindPropertyConnectedElementsLHS(), HFindPropertyCompleteLHS())

#    def test_verify_simple_property2(self):
#        transformation = [[HS2S(), HM2M()], [HSM2SM()]]
#        rulesIncludingBackLinks = [[],[transformation[1][0]]]   
#        s = SymbolicStateSpace(transformation, rulesIncludingBackLinks, self.backwardPatterns)
#        s.build_set()
#        s.verify_property()

if __name__ == "__main__":
    #import sys;sys.argv = ['', 'Test.test']
    unittest.main()